home *** CD-ROM | disk | FTP | other *** search
/ Languguage OS 2 / Languguage OS II Version 10-94 (Knowledge Media)(1994).ISO / language / lolli / readme < prev   
Text File  |  1994-10-29  |  4KB  |  85 lines
  1. % README for Lolli 0.701 -- Josh Hodas (hodas@saul.cis.upenn.edu) 11/30/92*
  2.  
  3. This distribution contains the files necessary to build an interpreter for
  4. a prolog-like language based on intuitionistic linear logic.
  5.  
  6. The language Lolli (named for the linear logic implication operator "-o"
  7. called lollipop), is a full implementation of the language described in
  8. our paper "Logic Programming in a Fragment of Intuitionistic Linear
  9. Logic" (Hodas & Miller, to appear in Information and Computation '92), 
  10. though it differs a bit in syntax, and has several built-in extra-logical 
  11. predicates and operators.**
  12.  
  13. This preliminary implementation was developed over the last year 
  14. and is based on code written by Frank Pfenning and Conal Elliot for their 
  15. excellent paper "A Semi-Functional Implementation of a Higher-Order Logic 
  16. Programming Language" which appears in "Topics in Advanced Language 
  17. Implementation" , MIT Press, Peter Lee editor.  The paper is also available 
  18. from CMU as Ergo Report 89-080. 
  19.  
  20. The system is written in Standard ML of New Jersey, and the parser and lexer
  21. were built using the parser-generator (MLYACC) and lexical-analyzer-generator
  22. (MLLEX) distributed with that system.  Though source files for the parser 
  23. and lexer have been included, the parser and lexer have already been built, 
  24. so you do not need access to the MLYACC or MLLEX.
  25.  
  26. For those who do not have SML-NJ at their site, I am attempting to provide
  27. pre-built binaries for a variety of architectures. These binaries will
  28. be stored in compressed form in the same directory (/pub/lolli) from
  29. which you ftp'ed this distribution. At present Sparc and NeXT binaries
  30. are available.  If you compile lolli on a new architecture, please contact me
  31. so that I can distribute your binary.
  32.  
  33.  
  34.  
  35. Contents of the Distribution
  36. ----------------------------
  37.  
  38. The ./src directory contains files used to build an executable version
  39. of Lolli using SML-NJ. It also contains the following two subdirectories
  40. which hold the source code for the system itself.
  41.  
  42.     ./src/parser contains the source grammar and lex files used to 
  43.     build the Lolli parser, as well as the code used to interface the 
  44.     parser to the main system.
  45.  
  46.     ./src/interpreter includes all the SML source code for the Lolli 
  47.     interpreter itself. The core of the prover is in 
  48.     ./src/interpreter/interprter.sml. The remaining files define the 
  49.     term and formula language, and give code for lifting terms to formulas.
  50.  
  51. The ./papers directory includes DVI and PostScript versions of several
  52. papers relating to Lolli, as well as a preliminary version of the 
  53. Elliot & Pfenning paper mentioned above.
  54.  
  55. The ./examples directory includes several sub-directories of example Lolli
  56. programs. Most are drawn from the papers mentioned above, but almost all
  57. have been changed to make use of some of the built-in predicates, to make them
  58. more functional.
  59.  
  60.  
  61. --------------------
  62. *Work on this project, by Josh Hodas and Dale Miller, has been funded by
  63. ONR N00014-88-K-0633, NSF CCR-87-05596, NSF CCR-91-02753, and DARPA 
  64. N00014-85-K-0018, through the University of Pennsylvania.  Miller was also 
  65. supported by SERC Grant No. GR/E 78487 "The Logical Framework" and ESPRIT 
  66. Basic Research Action No. 3245 "Logical Frameworks: Design Implementation 
  67. and Experiment" while he was visiting the University of Edinburgh.
  68.  
  69.  
  70. **The internal representation of formulas and proof contexts is
  71. actually based on an earlier version of the logic, described in the
  72. "extended abstract" version of the paper presented at the 1991 Logic
  73. In Computer Science conference (which paper is also include in this
  74. distribution). This distinction permeates aspects of the interpreter
  75. in subtle ways, but should not be apparent to the user. A future
  76. version of the system will likely shift to an internal representation
  77. more in line with the journal version of the paper.
  78.  
  79. More seriously, the interpreter implements a modified proof system that
  80. handles "TOP" lazily, rather than generating all possible subcontexts.
  81. A Latex file of the modified proof system is in the ./papers directory.
  82. The proof that it is sound and complete relative to the original system 
  83. has been completed, and will appear in my thesis.
  84.  
  85.